Search Results

Documents authored by Zeilberger, Noam

Document
DOI: 10.4230/LIPIcs.FSCD.2023.17
Convolution Products on Double Categories and Categorification of Rule Algebras

Authors: Nicolas Behr, Paul-André Melliès, and Noam Zeilberger

Published in: LIPIcs, Volume 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)

Abstract
Motivated by compositional categorical rewriting theory, we introduce a convolution product over presheaves of double categories which generalizes the usual Day tensor product of presheaves of monoidal categories. One interesting aspect of the construction is that this convolution product is in general only oplax associative. For that reason, we identify several classes of double categories for which the convolution product is not just oplax associative, but fully associative. This includes in particular framed bicategories on the one hand, and double categories of compositional rewriting theories on the other. For the latter, we establish a formula which justifies the view that the convolution product categorifies the rule algebra product.
Cite as

Nicolas Behr, Paul-André Melliès, and Noam Zeilberger. Convolution Products on Double Categories and Categorification of Rule Algebras. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 17:1-17:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{behr_et_al:LIPIcs.FSCD.2023.17,
  author =	{Behr, Nicolas and Melli\`{e}s, Paul-Andr\'{e} and Zeilberger, Noam},
  title =	{{Convolution Products on Double Categories and Categorification of Rule Algebras}},
  booktitle =	{8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
  pages =	{17:1--17:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-277-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{260},
  editor =	{Gaboardi, Marco and van Raamsdonk, Femke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.17},
  URN =		{urn:nbn:de:0030-drops-180017},
  doi =		{10.4230/LIPIcs.FSCD.2023.17},
  annote =	{Keywords: Categorical rewriting, double pushout, sesqui-pushout, double categories, convolution product, presheaf categories, framed bicategories, opfibrations, rule algebra}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2017.33
A Sequent Calculus for a Semi-Associative Law

Authors: Noam Zeilberger

Published in: LIPIcs, Volume 84, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)

Abstract
We introduce a sequent calculus with a simple restriction of Lambek's product rules that precisely captures the classical Tamari order, i.e., the partial order on fully-bracketed words (equivalently, binary trees) induced by a semi-associative law (equivalently, tree rotation). We establish a focusing property for this sequent calculus (a strengthening of cut-elimination), which yields the following coherence theorem: every valid entailment in the Tamari order has exactly one focused derivation. One combinatorial application of this coherence theorem is a new proof of the Tutte-Chapoton formula for the number of intervals in the Tamari lattice Y_n. Elsewhere, we have also used the sequent calculus and the coherence theorem to build a surprising bijection between intervals of the Tamari order and a natural fragment of lambda calculus, consisting of the beta-normal planar lambda terms with no closed proper subterms.
Cite as

Noam Zeilberger. A Sequent Calculus for a Semi-Associative Law. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 33:1-33:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{zeilberger:LIPIcs.FSCD.2017.33,
  author =	{Zeilberger, Noam},
  title =	{{A Sequent Calculus for a Semi-Associative Law}},
  booktitle =	{2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)},
  pages =	{33:1--33:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-047-7},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{84},
  editor =	{Miller, Dale},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.33},
  URN =		{urn:nbn:de:0030-drops-77179},
  doi =		{10.4230/LIPIcs.FSCD.2017.33},
  annote =	{Keywords: proof theory, combinatorics, coherence theorem, substructural logic, associativity}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact